Programmverifikation

1. Begriff der Informatik: (1) Formale Vorgehensweise mit dem Ziel, die Korrektheit eines ⇡ Programms bzw. ⇡ Moduls zu beweisen; (2) Forschungsgebiet, das sich mit Methoden des Korrektheitsbeweises beschäftigt.

- 2. Motivation: Da mit dem gebräuchlichen ⇡ Testen eines Programms die Korrektheit nicht garantiert werden kann, wurde nach Möglichkeiten gesucht, als Ersatz oder in Ergänzung die Korrektheit durch theoretische Analyse des Programmtexts zu beweisen.

- 3. Voraussetzungen: (1) Eine ⇡ formale Spezifikation der Aufgabe des Programms bzw. Moduls; (2) eine formale Beschreibung der ⇡ Semantik einer Programmiersprache.

- 4. Vorteil: Korrektheit wird bewiesen, nicht nur unterstellt wie beim Testen.

- 5. Nachteil: P. von Hand ist extrem aufwändig; lässt sich nur bei sehr kleinen Programmen anwenden, bei größeren Programmen nicht praktikabel. Intensive Forschungsbemühungen in der Informatik, die P. so weit wie möglich zu automatisieren.